w:world{i:l}. w-atom-constraint{i:l}(w)  Prop{i'} 

latex

Definitions	World, t  T, x:A. B(x), w.M, f(a), Type, AtomFree(T;x), Id, x:AB(x), Prop, IdLnk, w.TA, x:AB(x), P & Q, w.T, w-atom-constraint(w)
Lemmas	w-T wf, w-TA wf, IdLnk wf, Id wf, atom-free wf, w-M wf, world wf